@InProceedings{SantiagoJúniorTaha:2015:TiPeFo,
author = "Santiago J{\'u}nior, Valdivino Alexandre de and Tahar,
Sofi{\`e}ne",
affiliation = "{Instituto Nacional de Pesquisas Espaciais (INPE)} and {Concordia
University}",
title = "Time performance formal evaluation of complex systems",
year = "2015",
organization = "Congresso Brasileirod e Software: Teoria e Pr{\'a}tica",
abstract = "Formal verification methods, such as Model Checking, have been
used for addressing performance/dependability analysis of systems.
Such formal methods have several advantages over traditional
techniques aiming at performance/dependability analysis such as
the use of a single computational technique for evaluation of any
measure and all complex numerical computation steps are hidden to
the user. This paper reports on the use of Probabilistic Model
Checking for time performance evaluation of complex systems. We
propose an approach, TPerP, that allows a professional to clearly
address time performance analysis based on Continuous-Time Markov
Chain (CTMC). Our approach takes into consideration several types
of delay analyzes. We applied it to a balloonborne high energy
astrophysics scientific experiment where we dealt with CTMCs that
had around 30 million reachable states and 75 million transitions,
and we concluded that the current definition used in the balloon
system is inadequate in terms of performance.",
conference-location = "Belo Horizonte, MG",
conference-year = "21-25 set.",
language = "en",
urlaccessdate = "27 abr. 2024"
}